(define u0 (lambda (y) (lambda (x) x) (lambda (x) x)))
(define u1 (lambda (x) (lambda (x) x) (lambda (x) x)))
